| Definitions | Dsys, t  T, Unit, Type, Id, IdLnk, left+right,  , x:A  B(x),  x:A. B(x), M(i), M.state, locl(a), M.da(a), Feasible(D), d-comp-partial-world(D;v;sched;dec;t), queue(l;t), d-world(D;v;sched;dec), <a,b>, M.dout2(l;tg), Msg(M), type List, s = t, P   Q, False,  A, A B,  , {x:A| B(x) }, snds(l;t), rcvs(l;t), True,  T, nth_tl(n;as), source(l),  x.A(x), concat(ll), {i..j }, upto(n), #$n, M.dout(l,tg), P & Q, i j < k, w.M, Msg, m(l;t), d-partial-world(D;f;t';s), ||as||, Prop, a<b, Void, S  T, l[i], i j,  b, b,  , i<j, P  Q, x:A B(x), P Q, onlnk(l;mss), m(i;t), d-comp(D;v;sched;dec), CV(F), f(a), d-world-state(D;i), mlnk(m), M.Msg, a = b, filter(P;l), Msg(da), Action(i), a(i;t), map(f;as), destination(l), w-action-dec(TA;M;i), Action(dec), kind(a), isnull(a), w.TA, isrcv(l;a), false, Knd, x. t(x), lnk(k), 1of(t), isrcv(k), null, if b t else f fi |
| Lemmas | ifthenelse wf, null-action wf, w-a wf, action wf, assert of bnot, not wf, isrcv wf, lnk wf, pi1 wf, w-action-dec wf, Knd wf, bfalse wf, w-action wf, ldst wf, select upto, filter wf, eq lnk wf, mlnk wf, ma-msg wf, mlnk wf d, CV wf, d-comp wf2, d-world-state wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, bnot of lt int, assert of le int, lt int wf, bool wf, bnot wf, assert wf, le int wf, select wf, length wf1, length upto, d-comp-partial-world wf, w-ml wf, le wf, subtype rel list, w-Msg wf, d-world wf, subtype rel self, ma-dout wf, upto wf, int seg wf, map equal, concat wf, Msg wf, ma-dout2 wf, lsrc wf, nth tl wf, squash wf, true wf, d-feasible wf, ma-da wf, locl wf, ma-st wf, d-m wf, nat wf, IdLnk wf, Id wf, unit wf, dsys wf |
dec:(i,a:Id